the_es:ES, e', e:E. Dec((e < e')) 

latex

Definitions	x:A. B(x), t  T, , P  Q, x. t(x), P  Q, A c B, WellFnd{i}(A;x,y.R(x;y)), x(s), {T}, P  Q, P  Q, P & Q
Lemmas	es-causl-wellfnd, es-E wf, decidable wf, es-causl wf, decidable functionality, not wf, assert wf, es-first wf, es-pred wf, es-isrcv wf, es-sender wf, es-causl-iff, decidable or, event system wf, decidable cand, decidable not, decidable assert, es-pred-causl, decidable es-E-equal, es-sender-causl